fpf-all(A; eq; f; x,v.P(x;v)) == x:A. (fpf-dom(eq; x; f))  P(x;fpf-ap(f; eq; x)) 

latex

Definitions	fpf-all(A; eq; f; x,v.P(x;v)), x:A. B(x), P  Q, b, fpf-dom(eq; x; f), fpf-ap(f; eq; x)
FDL editor aliases	fpf-all